$\forall$$A_{1}$, $A_{2}$, $B_{1}$, $B_{2}$:Type.  $A_{1}$ $\sim$ $A_{2}$ $\Rightarrow$  $B_{1}$ $\sim$ $B_{2}$ $\Rightarrow$ ( $A_{1}$ $\sim$ $B_{1}$ $\Leftarrow\!\Rightarrow$  $A_{2}$ $\sim$ $B_{2}$)